DROPS

Document

DOI: 10.4230/LIPIcs.CSL.2021.34

Typable Fragments of Polynomial Automatic Amortized Resource Analysis

Authors: Long Pham and Jan Hoffmann

Published in: LIPIcs, Volume 183, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021)

Abstract

Being a fully automated technique for resource analysis, automatic amortized resource analysis (AARA) can fail in returning worst-case cost bounds of programs, fundamentally due to the undecidability of resource analysis. For programmers who are unfamiliar with the technical details of AARA, it is difficult to predict whether a program can be successfully analyzed in AARA. Motivated by this problem, this article identifies classes of programs that can be analyzed in type-based polynomial AARA. Firstly, it is shown that the set of functions that are typable in univariate polynomial AARA coincides with the complexity class PTime. Secondly, the article presents a sufficient condition for typability that axiomatically requires every sub-expression of a given program to be polynomial-time. It is proved that this condition implies typability in multivariate polynomial AARA under some syntactic restrictions.

Cite as

Long Pham and Jan Hoffmann. Typable Fragments of Polynomial Automatic Amortized Resource Analysis. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 34:1-34:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{pham_et_al:LIPIcs.CSL.2021.34,
  author =	{Pham, Long and Hoffmann, Jan},
  title =	{{Typable Fragments of Polynomial Automatic Amortized Resource Analysis}},
  booktitle =	{29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
  pages =	{34:1--34:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-175-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{183},
  editor =	{Baier, Christel and Goubault-Larrecq, Jean},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.34},
  URN =		{urn:nbn:de:0030-drops-134681},
  doi =		{10.4230/LIPIcs.CSL.2021.34},
  annote =	{Keywords: Resource consumption, Quantitative analysis, Amortized analysis, Typability}
}

Search Results

Documents authored by Pham, Long

Typable Fragments of Polynomial Automatic Amortized Resource Analysis

Abstract

Cite as

Thanks for your feedback!

Could not send message